0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 83 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 8 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 129 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 MRRProof (⇔, 29 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → U4_GA(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → APPA_IN_AAAG(X43, T26, X44, T25)
APPA_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → U1_AAAG(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
APPA_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APPA_IN_AAAG(X92, T52, X93, T51)
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_GA(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → APPC_IN_GGGA(T24, T31, T32, X9)
APPC_IN_GGGA(T87, T88, T89, .(T87, X151)) → U3_GGGA(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
APPC_IN_GGGA(T87, T88, T89, .(T87, X151)) → APPB_IN_GGA(T88, T89, X151)
APPB_IN_GGA(.(T105, T106), T107, .(T105, X181)) → U2_GGA(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
APPB_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APPB_IN_GGA(T106, T107, X181)
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_GA(T24, T25, T26, T33, permE_in_ga(T65, T33))
U7_GA(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U9_GA(T125, T126, T127, appD_in_ga(T126, X9))
PERME_IN_GA(.(T125, T126), .(T125, T127)) → APPD_IN_GA(T126, X9)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, appD_in_ga(T126, T128))
U10_GA(T125, T126, T127, appD_out_ga(T126, T128)) → U11_GA(T125, T126, T127, permE_in_ga(T128, T127))
U10_GA(T125, T126, T127, appD_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → U4_GA(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → APPA_IN_AAAG(X43, T26, X44, T25)
APPA_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → U1_AAAG(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
APPA_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APPA_IN_AAAG(X92, T52, X93, T51)
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_GA(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → APPC_IN_GGGA(T24, T31, T32, X9)
APPC_IN_GGGA(T87, T88, T89, .(T87, X151)) → U3_GGGA(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
APPC_IN_GGGA(T87, T88, T89, .(T87, X151)) → APPB_IN_GGA(T88, T89, X151)
APPB_IN_GGA(.(T105, T106), T107, .(T105, X181)) → U2_GGA(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
APPB_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APPB_IN_GGA(T106, T107, X181)
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_GA(T24, T25, T26, T33, permE_in_ga(T65, T33))
U7_GA(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U9_GA(T125, T126, T127, appD_in_ga(T126, X9))
PERME_IN_GA(.(T125, T126), .(T125, T127)) → APPD_IN_GA(T126, X9)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, appD_in_ga(T126, T128))
U10_GA(T125, T126, T127, appD_out_ga(T126, T128)) → U11_GA(T125, T126, T127, permE_in_ga(T128, T127))
U10_GA(T125, T126, T127, appD_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
APPB_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APPB_IN_GGA(T106, T107, X181)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
APPB_IN_GGA(.(T105, T106), T107, .(T105, X181)) → APPB_IN_GGA(T106, T107, X181)
APPB_IN_GGA(.(T105, T106), T107) → APPB_IN_GGA(T106, T107)
From the DPs we obtained the following set of size-change graphs:
APPA_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APPA_IN_AAAG(X92, T52, X93, T51)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
APPA_IN_AAAG(.(T50, X92), T52, X93, .(T50, T51)) → APPA_IN_AAAG(X92, T52, X93, T51)
APPA_IN_AAAG(.(T50, T51)) → APPA_IN_AAAG(T51)
From the DPs we obtained the following set of size-change graphs:
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, appD_in_ga(T126, T128))
U10_GA(T125, T126, T127, appD_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, appA_in_aaag(X43, T26, X44, T25))
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U4_ga(T24, T25, T26, T27, appA_out_aaag(X43, T26, X44, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, X9))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
U6_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, X9)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, appD_in_ga(T126, X9))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U9_ga(T125, T126, T127, appD_out_ga(T126, X9)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, appD_in_ga(T126, T128))
U10_ga(T125, T126, T127, appD_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, appA_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, appA_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, appC_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, appC_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, appD_in_ga(T126, T128))
U10_GA(T125, T126, T127, appD_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
appA_in_aaag(.(T50, X92), T52, X93, .(T50, T51)) → U1_aaag(T50, X92, T52, X93, T51, appA_in_aaag(X92, T52, X93, T51))
appA_in_aaag([], T60, T61, .(T60, T61)) → appA_out_aaag([], T60, T61, .(T60, T61))
appC_in_ggga(T87, T88, T89, .(T87, X151)) → U3_ggga(T87, T88, T89, X151, appB_in_gga(T88, T89, X151))
appD_in_ga(T131, T131) → appD_out_ga(T131, T131)
U1_aaag(T50, X92, T52, X93, T51, appA_out_aaag(X92, T52, X93, T51)) → appA_out_aaag(.(T50, X92), T52, X93, .(T50, T51))
U3_ggga(T87, T88, T89, X151, appB_out_gga(T88, T89, X151)) → appC_out_ggga(T87, T88, T89, .(T87, X151))
appB_in_gga(.(T105, T106), T107, .(T105, X181)) → U2_gga(T105, T106, T107, X181, appB_in_gga(T106, T107, X181))
appB_in_gga([], T113, T113) → appB_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X181, appB_out_gga(T106, T107, X181)) → appB_out_gga(.(T105, T106), T107, .(T105, X181))
PERME_IN_GA(.(T24, T25)) → U5_GA(T24, appA_in_aaag(T25))
U5_GA(T24, appA_out_aaag(T31, T26, T32)) → U7_GA(appC_in_ggga(T24, T31, T32))
U7_GA(appC_out_ggga(T65)) → PERME_IN_GA(T65)
PERME_IN_GA(.(T125, T126)) → U10_GA(appD_in_ga(T126))
U10_GA(appD_out_ga(T128)) → PERME_IN_GA(T128)
appA_in_aaag(.(T50, T51)) → U1_aaag(T50, appA_in_aaag(T51))
appA_in_aaag(.(T60, T61)) → appA_out_aaag([], T60, T61)
appC_in_ggga(T87, T88, T89) → U3_ggga(T87, appB_in_gga(T88, T89))
appD_in_ga(T131) → appD_out_ga(T131)
U1_aaag(T50, appA_out_aaag(X92, T52, X93)) → appA_out_aaag(.(T50, X92), T52, X93)
U3_ggga(T87, appB_out_gga(X151)) → appC_out_ggga(.(T87, X151))
appB_in_gga(.(T105, T106), T107) → U2_gga(T105, appB_in_gga(T106, T107))
appB_in_gga([], T113) → appB_out_gga(T113)
U2_gga(T105, appB_out_gga(X181)) → appB_out_gga(.(T105, X181))
appA_in_aaag(x0)
appC_in_ggga(x0, x1, x2)
appD_in_ga(x0)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
appB_in_gga(x0, x1)
U2_gga(x0, x1)
PERME_IN_GA(.(T24, T25)) → U5_GA(T24, appA_in_aaag(T25))
U5_GA(T24, appA_out_aaag(T31, T26, T32)) → U7_GA(appC_in_ggga(T24, T31, T32))
U7_GA(appC_out_ggga(T65)) → PERME_IN_GA(T65)
PERME_IN_GA(.(T125, T126)) → U10_GA(appD_in_ga(T126))
U10_GA(appD_out_ga(T128)) → PERME_IN_GA(T128)
appA_in_aaag(.(T50, T51)) → U1_aaag(T50, appA_in_aaag(T51))
appA_in_aaag(.(T60, T61)) → appA_out_aaag([], T60, T61)
appC_in_ggga(T87, T88, T89) → U3_ggga(T87, appB_in_gga(T88, T89))
appD_in_ga(T131) → appD_out_ga(T131)
U1_aaag(T50, appA_out_aaag(X92, T52, X93)) → appA_out_aaag(.(T50, X92), T52, X93)
U3_ggga(T87, appB_out_gga(X151)) → appC_out_ggga(.(T87, X151))
appB_in_gga(.(T105, T106), T107) → U2_gga(T105, appB_in_gga(T106, T107))
appB_in_gga([], T113) → appB_out_gga(T113)
U2_gga(T105, appB_out_gga(X181)) → appB_out_gga(.(T105, X181))
U10GA1 > appCinggga3 > U3ggga2 > U5GA2 > appBingga2 > U7GA1 > PERMEINGA1 > appAinaaag1 > U1aaag2 > U2gga2 > appCoutggga1 > appBoutgga1 > appAoutaaag3 > appDinga1 > appDoutga1 > [] > .2
[]=5
appA_in_aaag_1=3
appD_in_ga_1=2
appD_out_ga_1=1
appB_out_gga_1=5
appC_out_ggga_1=3
PERME_IN_GA_1=4
U7_GA_1=1
U10_GA_1=3
._2=2
U1_aaag_2=2
appA_out_aaag_3=0
appC_in_ggga_3=0
U3_ggga_2=0
appB_in_gga_2=0
U2_gga_2=2
U5_GA_2=0
appA_in_aaag(x0)
appC_in_ggga(x0, x1, x2)
appD_in_ga(x0)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
appB_in_gga(x0, x1)
U2_gga(x0, x1)